Inference at * 1 
Iof proof for Lemma all functionality wrt implies:



1. S : Type
2. T : Type
3. P : S
4. Q : S
5. S = T
6. z:S. P(z)  Q(z)
7. x:S. P(x)
8. y : T
  Q(y) 

latex

 by InteriorProof ((HypBackchain) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
CollapseTHEN ((Aut),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, P  Q, x:A. B(x)